Inference at * 1 1 3 1 
Iof proof for Lemma gen hyp tp:



1. A : Type
2. e : A
3. H : AType
4. H(e)
5. A  Type
6. e  A
7. x : A
  (e = x)  Type 

latex

 by MemberEqCD 

latex

 1: .....subterm..... T:t1:n

 1:   A  Type
 2: .....subterm..... T:t2:n

 2:   e  A
 3: .....subterm..... T:t3:n

 3:   x  A
 .

Definitions

t  T